Inference at * 
Iof proof for Lemma branch wf:


  P:, d:Dec(P), T:Type, A:(PT), B:T. if p:P then A(p) else B fi   T 

latex

 by (Auto) 
CollapseTHEN ((Unfold `branch` ( 0)) 
CollapseTHEN (Auto)) 

latex

C1: .....subterm..... T:t1:n

C1: 1. P : 
C1: 2. d : Dec(P)
C1: 3. T : Type
C1: 4. PT
C1: 5. T
C1:   d  (P + (P))
C.

Definitions

Type, if p:P then A(p) else B fi , case b of inl(x) => s(x) | inr(y) => t(y), x(s), f(a), , x:A. B(x), False, P  Q, x:AB(x), Void, t  T, left + right, A, Dec(P)